P:(), d:(n:. Dec(P(n))). (n:. P(n))  (mu(d)  ) 

latex

Definitions	mu(f), , t  T, f(a), #$n, {i..j}, x:A. B(x), P  Q, Dec(P), x:A. B(x), , x:AB(x), x:A  B(x), A  B, P & Q, i  j < k, {x:A| B(x)} , Type, i  j , False, A, -n, n+m, n - m, a < b, Void, b, , , x.A(x), if b then t else f fi , left + right, P  Q, s = t, {T}, SQType(T), s ~ t, True, T, x(s)
Lemmas	decidable int equal, ifthenelse wf, mu wf, ge wf, nat properties, nat wf, decidable wf, int seg wf, le wf